Jump to content

Lawvere theory

From Wikipedia, the free encyclopedia

In category theory, a Lawvere theory (named after American mathematician William Lawvere) is a category that can be considered a categorical counterpart of the notion of an equational theory.

Definition

[edit]

Let be a skeleton of the category FinSet of finite sets and functions. Formally, a Lawvere theory consists of a small category L with (strictly associative) finite products and a strict identity-on-objects functor preserving finite products.

A model of a Lawvere theory in a category C with finite products is a finite-product preserving functor M : LC. A morphism of models h : MN where M and N are models of L is a natural transformation of functors.

Category of Lawvere theories

[edit]

A map between Lawvere theories (LI) and (L′, I′) is a finite-product preserving functor that commutes with I and I′. Such a map is commonly seen as an interpretation of (LI) in (L′, I′).

Lawvere theories together with maps between them form the category Law.

Variations

[edit]

Variations include multisorted (or multityped) Lawvere theory, infinitary Lawvere theory, and finite-product theory.[1]

See also

[edit]

Notes

[edit]

References

[edit]
  • Hyland, Martin; Power, John (2007), "The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads" (PDF), Electronic Notes in Theoretical Computer Science, 172 (Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin): 437–458, CiteSeerX 10.1.1.158.5440, doi:10.1016/j.entcs.2007.02.019
  • Lawvere, William F. (1963), "Functorial Semantics of Algebraic Theories", PhD Thesis, vol. 50, no. 5, Columbia University, pp. 869–872, Bibcode:1963PNAS...50..869L, doi:10.1073/pnas.50.5.869, PMC 221940, PMID 16591125